1. $T$ : Type
\\[0ex]$\vdash$  $\forall$$h$, $f$:($T$$\rightarrow$($T$ + Top)). p{-}id() o $h$   = $h$